<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN"
 "http://www.w3.org/TR/html4/loose.dtd">
<!-- Uses "almost standards mode", all but some table cell sizing. -->
<html>
<head>
  <meta http-equiv="content-type" content="text/html; charset=UTF-8">
  <title>Prooftoys</title>
  <link id=styles type="text/css" rel="stylesheet" href="logic.css">
  <script src="boilerplate.js"></script>

<style type="text/css">
/* CSS here */
</style>

</head>
<body>

<h1>Prooftoys</h1>

<div id=slogans>
<!-- slogans here -->
</div>

<span id=leftNav>
<!-- Boilerplate text goes here -->
</span>

<span id=content>
<h2>About Prooftoys</h2>

<h3>The mission</h3>
Prooftoys is an open-source effort to use the Web to bring
user-friendly full-fledged logical reasoning tools to anyone who works
with math.  The current components are the engine and the user
interface.  They are both under continuing development and important
work remains to be done on both, but are available for experimental use.

<h3>Introduction</h3>
<p>
Prooftoys in its current form can be used in two rather different but
related ways.  It can be used to explore and create simple proofs in
mathematical logic.  Or it can be used as a tool to help in solving
basic algebra problems.

<h3>Algebra in Prooftoys</h3>
<p>
For practice with algebra problem solving, try the
<a href="http://mathtoys.org">Mathtoys</a> website.  That site is powered by the
same Prooftoys software that powers this one, but the
<a href="http://mathtoys.org">Mathtoys</a> site is dedicated to
helping you solve algebra problems.

<h3>Logic in Prooftoys</h3>
<p>
The <a href=booleans.html>Basic Logic through Pictures</a>, is an
introduction to some fundamental ideas of classical logic with
interactive illustrations.
<p>
The <a href=introduction.html>Introduction to Proofs</a> page is a
good first step toward reading Prooftoys proofs and building your own.
<p>
There is quite a bit more yet to be said about the logic as well.
Fortunately the logic and inference steps are quite standard, so any
part that looks familiar should work for you in textbook fashion.

<h3>The user interface</h3>
<p>
In the web-based Proof Builder user interface you can select steps,
expressions, and locations in steps by pointing and clicking, and
apply any predefined or extended public inference rule.  When reading
an existing proof you can drill down into the details of high-level
inference steps or theorems to see how they are proved in more detail.

<h3>The engine</h3>
The Prooftoys inference engine uses <i>higher-order logic</i>, which
means it can reason about functions and predicates, which themselves
can have functions and predicates as inputs and outputs.  This gives
it the power to help you develop as much of mathematics as you wish.
The engine runs directly in your web browser for best responsiveness,
interactivity, and convenient access to servers in the Internet cloud.
<p>
The engine implements a variant of Professor Peter B. Andrews'
<a href="http://en.wikipedia.org/wiki/Q_zero" target=_blank>
Q<sub>0</sub></a>, a version of higher-order logic with a small,
simple, and understandable kernel.  On this base it builds <i
 href="http://en.wikipedia.org/wiki/Natural_deduction">natural
deduction</i>-style reasoning and a variety high-level inference rules
that make it easy to build high-level proofs.
<p>
The engine is safely programmable, and you can create new high-level
inference rules without compromising correctness.

<h3>Further steps</h3>
<p>
The <a href=proofbuilder.html>Proof builder</a> is also available on a
standalone page.
<p>
Note: <i>Proof displays and the proof builder are supported in recent
versions of Firefox and Chrome.</i>
<p>
<a href="http://www.amazon.com/Introduction-Mathematical-Logic-Type-Theory/dp/9048160790/"
 target=_blank>An Introduction to Mathematical Logic and Type Theory</a>
by Professor Andrews contains a rigorous presentation of the full
logic implemented here among other logical topics.

</span> <!-- content -->

<script>

// Insert boilerplate.
Toy.insertNav();
Toy.insertSlogans();

</script>
</body>
</html>
